{-# LANGUAGE TypeFamilies, TypeOperators, MultiParamTypeClasses,
  FlexibleContexts, FlexibleInstances, UndecidableInstances,
  ScopedTypeVariables  #-}

{-# OPTIONS_GHC -fcontext-stack=250 #-}

module CnvRelSingly (HCompos(..)) where

import TypeBasics
import Yoko



import Control.Applicative





instance HCompos s sum t => HCompos s (DCsOf s sum) t where
  hcompos cnv = hcompos cnv . unDCsOf





class HCompos s rep t where
  hcompos :: Applicative i => (s -> i t) -> rep -> i t





instance (HCompos s a t, HCompos s b t
         ) => HCompos s (a :+: b) t where
  hcompos cnv = foldPlus (hcompos cnv) (hcompos cnv)

-- NB only works if there's exactly one matching constructor
instance (Generic dc, Just (N dc') ~ FindDCs (Tag dc) (DCs t),
          MapRs s t (Rep dc) (Rep dc'),
          DC dc', Range dc' ~ t
         ) => HCompos s (N dc) t where
  hcompos cnv = 
    foldN $ fmap (rejoin . (id :: dc' -> dc') . obj) . mapRs cnv . rep



type family FindDCs s sum
type instance FindDCs s (N dc) =
  If (Equal s (Tag dc)) (Just (N dc)) Nothing
type instance FindDCs s (a :+: b) = DistMaybePlus (FindDCs s a) (FindDCs s b)



-- applies cnv to every Rec in a product; identity on other factors
class MapRs s t prod prod' where
  mapRs :: Applicative i => (s -> i t) -> prod -> i prod'

instance MapRs s t (Rec s) (Rec t) where
  mapRs cnv (Rec x) = Rec <$> cnv x

instance MapRs s t (Dep a) (Dep a) where mapRs _ = pure
instance MapRs s t U       U       where mapRs _ = pure

instance (MapRs s t a a', MapRs s t b b'
         ) => MapRs s t (a :*: b) (a' :*: b') where
  mapRs cnv (a :*: b) =
    (:*:) <$> mapRs cnv a <*> mapRs cnv b
